118 VI HUBERT SPACES

(6.2.3) (Minkowski's inequality) Iff is a positive hermitian form, then

(f(x + y,x + y))112 < (f(x9 *))1/2 + (f(y, y*))112
for any pair of vectors x, y in E.

As f(x + y, x + y) =f(x, x) +f(x, y} +/0, y) +f(y, y)9 the inequality is
equivalent to

9 y) =/(x, y) +f(x9y) < 2(f(x, x)f(y9 y))112
which follows from Cauchy-Schwarz.

The function x -> (f(x9 #))1/2 therefore satisfies the conditions (I), (III),
and (IV) of (Section 5.1); by (6.2.2), condition (II) of Section 5.1 is equivalent
to the fact that the form / is nondegenerate. Therefore, when / is a nonde-
generate positive hermitian form (also called a positive definite form),
(f(x9 x)Y/2 is a norm on E. A. prehilbert space is a vector space E with a given
nondegenerate positive hermitian form on E; when no confusion arises, that
form is written (x\y) and its value is called the scalar product of x and;;;
we always consider a prehilbert space E as a normed space, with the norm
||jc|| = (x\ x)i/29 and of course, such a space is always considered as a metric
space for the corresponding distance \\x — y\\. With these notations, the
Cauchy-Schwarz inequality is written

(6.2.4) \(x\y)\ ^ |l*|| - \\y\\

and this proves, by (5.5.1), that for a real prehilbert space E, (x9 y) -*(x\y)
is a continuous bilinear form on E x E (the argument of (5.5.1) can also be
applied when E is a complex prehilbert space and proves again the con-
tinuity of (x9y)-+(x\y)9 although this is not a bilinear form any more).
We also have, as a particular case of (6.1.1):

(6.2.5) (Pythagoras' theorem) In a prehilbert space E, ifx9 y are orthog-
onal vectors,

An isomorphism of a prehilbert space E onto a prehilbert space E' is
a linear bijection of E onto E' such that (f(x) |/0>)) = (x I y) for any pair
of vectors x, y of E. It is clear that an isomorphism is a linear isometry
of E onto E'.

Let E be a prehilbert space; then, on any vector subspace F of E, the
restriction of the scalar product is a positive nondegenerate hermitian form;
unless the contrary is stated, it is always that restriction which is meant when
F is considered as a prehilbert space.theorem (5.9.4).)